feat(Automata): Two-way automaton - #834
Conversation
crei
changed the title
| automaton can move from state `q` to state `q'` and move its head according to `m`. -/ | ||
| Tr (q : State) (x : Symbol) (m : SignType) (q' : State) : Prop | ||
| /-- The set of initial states of the automaton. -/ | ||
| start : Set State |
There was a problem hiding this comment.
Why do you want a set of starting and accepting states and not a single starting and single accpting state?
There was a problem hiding this comment.
That's just Vardi's definition. In the end, it doesn't really matter much, but this is also how NA is defined.
There was a problem hiding this comment.
I think you should take advantage of the LTS infrastructure in cslib. The state space of your LTS is TwoNACfg State input, the label space can be either Unit (if you don't really care about transition labels) or Symbol × SignType (if you want to expose the symbol being consumed and the head movement in transition labels), the Tr is Step a input. Then you can leverage the various notions of execution in cslib's LTS, such as LTS.MTr, LTS.Execution, and the InChainFromTo without having to develop your own.
Here's what I mean:
@[ext]
structure TwoNAState (State Symbol : Type*) (input : List Symbol) where
state : State
pos : Fin (input.length + 1)
def TwoNATrType (State Symbol : Type*) := State → Symbol → SignType → State → Prop
def TwoNALTS (input : List Symbol) (twoTr : TwoNATrType State Symbol) :
LTS (TwoNAState State Symbol input) Unit where
Tr c _ c' := ∃ m, ∃ _ : (c.pos : ℕ) < input.length,
twoTr c.state input[c.pos] m c'.state ∧ (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
def TwoNA (input : List Symbol) (twoTr : TwoNATrType State Symbol)
(start : Set ((TwoNAState State Symbol input))) :
Automata.NA (TwoNAState State Symbol input) Unit where
Tr := (TwoNALTS input twoTr).Tr
start := start
Then you don't need TwoNA-specific notions of executions; you can just use those in LTS and NA and all the theorems which have been proved about them.
|
Hi @crei and @SamuelSchlesinger, what do you think of @ctchou's comment? Does it match your goals? |
|
I changed this so that a TwoNA is now an NA with a specific label type. I'm still unsure if LTS is the right base here. As mentioned by @ctchou , there are two options about the label type:
The first one (as done in the comment above) requires you to define an LTS on top of the configurations and then only re-use MTr, but I think there is a lot of confusion because you have two different The second one (as done in the current state of the PR) cannot use Both of them cannot simply use the In general, I have the impression that you can do this with LTS, but the question is if you should. Already the fact that there is no clear winner between the two ways to define it might be an indication that the LTS model is not really fitting. It does provide the tools, but maybe a more basic notion like IsChainFromTo could provide the same tools? |
|
Actually the way it is now is wrong, because it inherits |
|
I tried it differently, closer to @ctchou 's suggestion. Basically starting with an LTS on the Configurations and restricting the transitions by disallowing the illegal labels such that |
|
Ok, this might be getting closer to a solution we can all agree on. I now defined My main criticism still stands, you have to dig a bit into the definitions of LTS to be able to judge that this definition is equivalent to the one given in Vardi's paper. As an alternative, I gave one that is closer to the paper and uses |
|
How about I give it a try myself? I don't have time right now, but should have enough time in the next 48 hours or so. My current guess is this:
|
|
I just pushed an alternative design of 2-way automata in a new file |
|
What I like about your version is the fact that the equality on inputs is enforced on the configuration level, at the point where you restrict the transition relation. I'm not so happy about the fact that the original transition relation is not visible any more and also the initial states are not available. I also see that "TwoWayNA" makes much more sense as a name, but I won't change that for now to not complicate the diff. I agree that an LTS without labels does not really make sense. Let me try to move the input into the configurations. |
There was a problem hiding this comment.
I see what you are doing in the via LTS section. I think it can probably work, in the sense of allowing you to leverage the results already proved for LTS. But note that the read pointer pos and the input should really be considered an integral part of the state of a 2-way automaton. But they are not part of your definition of TwoNA. You "slip them in" later in TwoNA.toCfgTr. But this is ultimately an aesthetic judgement on my part and I won't insist on it.
To make my point above more provocatively, notice that TwoNA could be interpreted as (the finite-state control of) a 1-tape Turing machine. All you have to do is to use a product type Symbol x Symbol for the Symbol in TwoNATr and interpret the first component of the product as the symbol read from the tape and the second the symbol written to the tape. Because the state of your TwoNA does not include the tape, you don't get an opportunity to state the invariant that the tape is not allowed to change in TwoNA.
| def TwoNATr.toCfgTr {State Symbol : Type*} (tr : TwoNATr State Symbol) : | ||
| TwoNACfg State Symbol → Symbol × SignType → TwoNACfg State Symbol → Prop | ||
| | c, (x, m), c' => | ||
| c.input = c'.input ∧ | ||
| some x = c.input[c.pos]? ∧ | ||
| tr c.state x m c'.state ∧ | ||
| (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ) | ||
|
|
||
| def TwoNA.toCfgLTS {State Symbol : Type*} (a : TwoNA State Symbol) (input : List Symbol) : |
There was a problem hiding this comment.
I would suggest you rename .toCfgTr to .toCfgLTS and .toCfgLTS to .toCfgNAFinAcc. In fact, you can make .toCfgTr to return LTS (TwoNACfg State Symbol) (Symbol × SignType) to match its new name.
| state : State | ||
| /-- The input head position of the automaton: it can be on any symbol of the input or on the | ||
| position one step to the right of the input. -/ | ||
| pos : Fin (input.length + 1) |
There was a problem hiding this comment.
Personally I think it is more convenient to define pos : ℕ, because I found dealing with Fin types a pain in general. In the the transition relation you will have to somehow say that pos is within the index range of input in any case (namely, some x = c.input[c.pos]?).
|
Maybe it's just an aesthetic judgment but maybe I also don't understand. To me, the input head position cannot be part of the state, it can only be part of the configuration: All possible state sets and all possible transitions (allowed by the type system) should be valid. The restriction comes in when we are talking about the "implementation details" of the automaton and what it means for it to accept a word and transition between configurations. For me, it is important to ensure in the type system that it is not possible to construct an 'illegal' TwoWayNA, because only then can we talk about what "any TwoWayNA" can do. In your alternative, |
ctchou
left a comment
ctchou
left a comment
There was a problem hiding this comment.
For me, a "state" of a machine is a complete summary of the past behavior of the machine and its future behavior should not depend on anything beyond what is in the "state". Call it a "configuration" if you like, but the point is that the computing power of a machine is determined by its "state" in the above sense, not just its "finite-state control" part. For example, you cannot define the correct Acceptor without referring to the complete "state". But, as I said, this is mostly an aesthetic issue and I won't insist on it.
| c.input = c'.input ∧ | ||
| some x = c.input[c.pos]? ∧ | ||
| a.Tr c.state x m c'.state ∧ | ||
| (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ) |
There was a problem hiding this comment.
I think it is clearer to not involve ℤ at all. For example, what happens if c.pos = 0 and m = neg? It would seem that the RHS is then -1 : ℤ. Does this force c'.pos to be 0? It takes some thinking and looking up the manual to figure that out. Why not spell it out via case splitting on m and (if necessary) c.pos?
[Edit] Actually it is worse than I thought, because you can prove this:
example (n : ℕ) (p : Fin n) : (p : ℤ) ≠ (0 : ℤ) + (SignType.neg : ℤ) := by simp
That is, if c.pos = 0 and m = neg, there is no next step. Is this what you want?
There was a problem hiding this comment.
Yes, this is exactly what I want, see the Implementation notes. This is also the way it is stated in the paper I'm formalizing here.
There was a problem hiding this comment.
The informal text of your implementation note allows at least two interpretations when c.pos = 0 and m = neg:
(1) there is no next configuration and hence the execution gets stuck at this point.
(2) there is a next configuration but pos stays at position 0.
Both approaches are reasonable in the sense that both will result in a regular language being accepted. Your code does (1), but that is not transparent. I had to squint hard at it and prove a theorem to be certain that my understanding is correct. You should spell out what you want either in the code or in the comment.
There was a problem hiding this comment.
I added more comments.
There was a problem hiding this comment.
Thanks for adding the clarifying comment. You can actually define an invariant and prove that it is indeed an invariant in the sense of LTS.TrInv and LTS.MTrInv as theorems.
5 participants
This defines a (nondeterministic) two-way automaton, i.e. an automaton with an input tape that can move its input tape head in both directions, following the definition by [Vardi1989]. The purpose of introducing two-way automata is to prove the power of Turing machines with constant space following Vardi's proof of equivalence of two-way and one-way automata.
The definition is not via LTS mainly because the labels would not coincide with the input symbols, which makes it a bit more awkward. Instead, this defines a single-step relation between configurations and then
List.IsChainis used to define a "Run", e.g. a sequence of configurations such that adjacent ones are Step-related and which starts at an initial configuration.